pnueli-zuck.5.jani:model: info: pnueli-zuck.5 is an MDP model and will be simulated as an MDP.
pnueli-zuck.5.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.5.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.5.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.5.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.5.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.5.jani: info: Using default value of 0.95 for the confidence parameter.
Peak memory usage: 65 MB
Analysis results for pnueli-zuck.5.jani
Status: Finished
Simulation time: 599.8 s
+ Property Property "live"
Estimated max. probability: 1
Runs used (best scheduler): 250
Total runs used: 128073850
Schedulers sampled: 127000
Best scheduler: 1067652374
Run type: MDP
Status: Finished
+ Error bounds
Scheduler sampling: The result is a lower bound for the true max. probability.
Statement: Adaptive: P(error > εp̂) < δ
ε: 0.02
δ: 0.050000000000000044